Termination proof of /tmp/tmp62LtYS/A16.itrs

Termination of the given ITRSProblem could not be shown:

↳ ITRS

  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

length(cons(x, l)) → +@z(1@z, length(l))
tail(nil) → nil
length(nil) → 0@z
cond(FALSE, n, l) → tail(nthtail(+@z(n, 1@z), l))
cond(TRUE, n, l) → l
nthtail(n, l) → cond(>=@z(n, length(l)), n, l)
tail(cons(x, l)) → l

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(FALSE, x0, x1)
cond(TRUE, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

Added dependency pairs

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

length(cons(x, l)) → +@z(1@z, length(l))
tail(nil) → nil
length(nil) → 0@z
cond(FALSE, n, l) → tail(nthtail(+@z(n, 1@z), l))
cond(TRUE, n, l) → l
nthtail(n, l) → cond(>=@z(n, length(l)), n, l)
tail(cons(x, l)) → l

The integer pair graph contains the following rules and edges:

(0): LENGTH(cons(x[0], l[0])) → LENGTH(l[0])
(1): COND(FALSE, n[1], l[1]) → NTHTAIL(+@z(n[1], 1@z), l[1])
(2): COND(FALSE, n[2], l[2]) → TAIL(nthtail(+@z(n[2], 1@z), l[2]))
(3): NTHTAIL(n[3], l[3]) → COND(>=@z(n[3], length(l[3])), n[3], l[3])
(4): NTHTAIL(n[4], l[4]) → LENGTH(l[4])

(0) -> (0), if ((l[0] →^* cons(x[0]a, l[0]a)))

(1) -> (3), if ((l[1] →^* l[3])∧(+@z(n[1], 1@z) →^* n[3]))

(1) -> (4), if ((l[1] →^* l[4])∧(+@z(n[1], 1@z) →^* n[4]))

(3) -> (1), if ((n[3] →^* n[1])∧(l[3] →^* l[1])∧(>=@z(n[3], length(l[3])) →^* FALSE))

(3) -> (2), if ((n[3] →^* n[2])∧(l[3] →^* l[2])∧(>=@z(n[3], length(l[3])) →^* FALSE))

(4) -> (0), if ((l[4] →^* cons(x[0], l[0])))

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(FALSE, x0, x1)
cond(TRUE, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

            ↳ UsableRulesProof

          ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

length(cons(x, l)) → +@z(1@z, length(l))
tail(nil) → nil
length(nil) → 0@z
cond(FALSE, n, l) → tail(nthtail(+@z(n, 1@z), l))
cond(TRUE, n, l) → l
nthtail(n, l) → cond(>=@z(n, length(l)), n, l)
tail(cons(x, l)) → l

The integer pair graph contains the following rules and edges:

(0): LENGTH(cons(x[0], l[0])) → LENGTH(l[0])

(0) -> (0), if ((l[0] →^* cons(x[0]a, l[0]a)))

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(FALSE, x0, x1)
cond(TRUE, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPNonInfProof

          ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph contains the following rules and edges:

(0): LENGTH(cons(x[0], l[0])) → LENGTH(l[0])

(0) -> (0), if ((l[0] →^* cons(x[0]a, l[0]a)))

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(FALSE, x0, x1)
cond(TRUE, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair LENGTH(cons(x[0], l[0])) → LENGTH(l[0]) the following chains were created:

We consider the chain LENGTH(cons(x[0], l[0])) → LENGTH(l[0]), LENGTH(cons(x[0], l[0])) → LENGTH(l[0]), LENGTH(cons(x[0], l[0])) → LENGTH(l[0]) which results in the following constraint:
(1)    (l[0]1=cons(x[0]2, l[0]2)∧l[0]=cons(x[0]1, l[0]1) ⇒ LENGTH(cons(x[0]1, l[0]1))≥LENGTH(l[0]1)∧(U^Increasing(LENGTH(l[0]1)), ≥))

We simplified constraint (1) using rule (III) which results in the following new constraint:
(2)    (LENGTH(cons(x[0]1, cons(x[0]2, l[0]2)))≥LENGTH(cons(x[0]2, l[0]2))∧(U^Increasing(LENGTH(l[0]1)), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    ((U^Increasing(LENGTH(l[0]1)), ≥)∧0 ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    ((U^Increasing(LENGTH(l[0]1)), ≥)∧0 ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    ((U^Increasing(LENGTH(l[0]1)), ≥)∧0 ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 = 0∧0 = 0∧(U^Increasing(LENGTH(l[0]1)), ≥)∧0 ≥ 0∧0 = 0)

To summarize, we get the following constraints P_≥ for the following pairs.

LENGTH(cons(x[0], l[0])) → LENGTH(l[0])
- (0 = 0∧0 = 0∧(U^Increasing(LENGTH(l[0]1)), ≥)∧0 ≥ 0∧0 = 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(cons(x₁, x₂)) = 1 + x₂
POL(LENGTH(x₁)) = -1 + x₁
POL(TRUE) = 0
POL(FALSE) = 0
POL(undefined) = 0

The following pairs are in P_>:

LENGTH(cons(x[0], l[0])) → LENGTH(l[0])

The following pairs are in P_bound:

LENGTH(cons(x[0], l[0])) → LENGTH(l[0])

The following pairs are in P_≥:
none

There are no usable rules.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPNonInfProof

                  ↳ IDP

                    ↳ IDependencyGraphProof

          ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph is empty.
The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(FALSE, x0, x1)
cond(TRUE, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

length(cons(x, l)) → +@z(1@z, length(l))
tail(nil) → nil
length(nil) → 0@z
cond(FALSE, n, l) → tail(nthtail(+@z(n, 1@z), l))
cond(TRUE, n, l) → l
nthtail(n, l) → cond(>=@z(n, length(l)), n, l)
tail(cons(x, l)) → l

The integer pair graph contains the following rules and edges:

(1): COND(FALSE, n[1], l[1]) → NTHTAIL(+@z(n[1], 1@z), l[1])
(3): NTHTAIL(n[3], l[3]) → COND(>=@z(n[3], length(l[3])), n[3], l[3])

(1) -> (3), if ((l[1] →^* l[3])∧(+@z(n[1], 1@z) →^* n[3]))

(3) -> (1), if ((n[3] →^* n[1])∧(l[3] →^* l[1])∧(>=@z(n[3], length(l[3])) →^* FALSE))

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(FALSE, x0, x1)
cond(TRUE, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

length(cons(x, l)) → +@z(1@z, length(l))
length(nil) → 0@z

The integer pair graph contains the following rules and edges:

(1): COND(FALSE, n[1], l[1]) → NTHTAIL(+@z(n[1], 1@z), l[1])
(3): NTHTAIL(n[3], l[3]) → COND(>=@z(n[3], length(l[3])), n[3], l[3])

(1) -> (3), if ((l[1] →^* l[3])∧(+@z(n[1], 1@z) →^* n[3]))

(3) -> (1), if ((n[3] →^* n[1])∧(l[3] →^* l[1])∧(>=@z(n[3], length(l[3])) →^* FALSE))

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(FALSE, x0, x1)
cond(TRUE, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

Represented integers and predefined function symbols by Terms

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, n[1], l[1]) → NTHTAIL(plus_int(pos(s(0)), n[1]), l[1])
NTHTAIL(n[3], l[3]) → COND(greatereq_int(n[3], length(l[3])), n[3], l[3])

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(false, x0, x1)
cond(true, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, n[1], l[1]) → NTHTAIL(plus_int(pos(s(0)), n[1]), l[1])
NTHTAIL(n[3], l[3]) → COND(greatereq_int(n[3], length(l[3])), n[3], l[3])

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
tail(nil)
length(nil)
cond(false, x0, x1)
cond(true, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

tail(nil)
cond(false, x0, x1)
cond(true, x0, x1)
nthtail(x0, x1)
tail(cons(x0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

COND(false, n[1], l[1]) → NTHTAIL(plus_int(pos(s(0)), n[1]), l[1])
NTHTAIL(n[3], l[3]) → COND(greatereq_int(n[3], length(l[3])), n[3], l[3])

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
In the following pairs the term without variables pos(s(0)) is replaced by the fresh variable x_removed.
Pair: COND(false, n[1], l[1]) → NTHTAIL(plus_int(pos(s(0)), n[1]), l[1])
Positions in right side of the pair:

[0,0]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                              ↳ QDP

                            ↳ RemovalProof

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

COND(false, n[1], l[1], x_removed) → NTHTAIL(plus_int(x_removed, n[1]), l[1], x_removed)
NTHTAIL(n[3], l[3], x_removed) → COND(greatereq_int(n[3], length(l[3])), n[3], l[3], x_removed)

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

[0,0]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                              ↳ QDP

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

COND(false, n[1], l[1], x_removed) → NTHTAIL(plus_int(x_removed, n[1]), l[1], x_removed)
NTHTAIL(n[3], l[3], x_removed) → COND(greatereq_int(n[3], length(l[3])), n[3], l[3], x_removed)

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule NTHTAIL(n[3], l[3]) → COND(greatereq_int(n[3], length(l[3])), n[3], l[3]) at position [0] we obtained the following new rules [LPAR04]:

NTHTAIL(y0, nil) → COND(greatereq_int(y0, pos(0)), y0, nil)
NTHTAIL(y0, cons(x0, x1)) → COND(greatereq_int(y0, plus_int(pos(s(0)), length(x1))), y0, cons(x0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

COND(false, n[1], l[1]) → NTHTAIL(plus_int(pos(s(0)), n[1]), l[1])
NTHTAIL(y0, nil) → COND(greatereq_int(y0, pos(0)), y0, nil)
NTHTAIL(y0, cons(x0, x1)) → COND(greatereq_int(y0, plus_int(pos(s(0)), length(x1))), y0, cons(x0, x1))

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [LPAR04] the rule COND(false, n[1], l[1]) → NTHTAIL(plus_int(pos(s(0)), n[1]), l[1]) we obtained the following new rules [LPAR04]:

COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)
COND(false, z0, cons(z1, z2)) → NTHTAIL(plus_int(pos(s(0)), z0), cons(z1, z2))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(y0, nil) → COND(greatereq_int(y0, pos(0)), y0, nil)
NTHTAIL(y0, cons(x0, x1)) → COND(greatereq_int(y0, plus_int(pos(s(0)), length(x1))), y0, cons(x0, x1))
COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)
COND(false, z0, cons(z1, z2)) → NTHTAIL(plus_int(pos(s(0)), z0), cons(z1, z2))

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                          ↳ RemovalProof

                                          ↳ RemovalProof

                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

COND(false, z0, cons(z1, z2)) → NTHTAIL(plus_int(pos(s(0)), z0), cons(z1, z2))
NTHTAIL(y0, cons(x0, x1)) → COND(greatereq_int(y0, plus_int(pos(s(0)), length(x1))), y0, cons(x0, x1))

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
In the following pairs the term without variables pos(s(0)) is replaced by the fresh variable x_removed.
Pair: COND(false, z0, cons(z1, z2)) → NTHTAIL(plus_int(pos(s(0)), z0), cons(z1, z2))
Positions in right side of the pair:

[0,0]

Pair: NTHTAIL(y0, cons(x0, x1)) → COND(greatereq_int(y0, plus_int(pos(s(0)), length(x1))), y0, cons(x0, x1))
Positions in right side of the pair:

[0,1,0]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                          ↳ RemovalProof

                                            ↳ QDP

                                          ↳ RemovalProof

                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

COND(false, z0, cons(z1, z2), x_removed) → NTHTAIL(plus_int(x_removed, z0), cons(z1, z2), x_removed)
NTHTAIL(y0, cons(x0, x1), x_removed) → COND(greatereq_int(y0, plus_int(x_removed, length(x1))), y0, cons(x0, x1), x_removed)

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

[0,0]

Pair: NTHTAIL(y0, cons(x0, x1)) → COND(greatereq_int(y0, plus_int(pos(s(0)), length(x1))), y0, cons(x0, x1))
Positions in right side of the pair:

[0,1,0]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                          ↳ RemovalProof

                                          ↳ RemovalProof

                                            ↳ QDP

                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

COND(false, z0, cons(z1, z2), x_removed) → NTHTAIL(plus_int(x_removed, z0), cons(z1, z2), x_removed)
NTHTAIL(y0, cons(x0, x1), x_removed) → COND(greatereq_int(y0, plus_int(x_removed, length(x1))), y0, cons(x0, x1), x_removed)

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)
NTHTAIL(y0, nil) → COND(greatereq_int(y0, pos(0)), y0, nil)

The TRS R consists of the following rules:

length(cons(x, l)) → plus_int(pos(s(0)), length(l))
length(nil) → pos(0)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)
NTHTAIL(y0, nil) → COND(greatereq_int(y0, pos(0)), y0, nil)

The TRS R consists of the following rules:

greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

length(cons(x0, x1))
length(nil)
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

length(cons(x0, x1))
length(nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)
NTHTAIL(y0, nil) → COND(greatereq_int(y0, pos(0)), y0, nil)

The TRS R consists of the following rules:

greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule NTHTAIL(y0, nil) → COND(greatereq_int(y0, pos(0)), y0, nil) at position [0] we obtained the following new rules [LPAR04]:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
NTHTAIL(pos(x0), nil) → COND(true, pos(x0), nil)
NTHTAIL(neg(0), nil) → COND(true, neg(0), nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)
NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
NTHTAIL(pos(x0), nil) → COND(true, pos(x0), nil)
NTHTAIL(neg(0), nil) → COND(true, neg(0), nil)

The TRS R consists of the following rules:

greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)

The TRS R consists of the following rules:

greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule COND(false, z0, nil) → NTHTAIL(plus_int(pos(s(0)), z0), nil) at position [0] we obtained the following new rules [LPAR04]:

COND(false, neg(x1), nil) → NTHTAIL(minus_nat(s(0), x1), nil)
COND(false, pos(x1), nil) → NTHTAIL(pos(plus_nat(s(0), x1)), nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, neg(x1), nil) → NTHTAIL(minus_nat(s(0), x1), nil)
COND(false, pos(x1), nil) → NTHTAIL(pos(plus_nat(s(0), x1)), nil)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, neg(x1), nil) → NTHTAIL(minus_nat(s(0), x1), nil)
NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, neg(x1), nil) → NTHTAIL(minus_nat(s(0), x1), nil)
NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)

The TRS R consists of the following rules:

minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

COND(false, neg(x1), nil) → NTHTAIL(minus_nat(s(0), x1), nil)
NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)

The TRS R consists of the following rules:

minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))

The set Q consists of the following terms:

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [LPAR04] the rule COND(false, neg(x1), nil) → NTHTAIL(minus_nat(s(0), x1), nil) we obtained the following new rules [LPAR04]:

COND(false, neg(s(z0)), nil) → NTHTAIL(minus_nat(s(0), s(z0)), nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, neg(s(z0)), nil) → NTHTAIL(minus_nat(s(0), s(z0)), nil)

The TRS R consists of the following rules:

minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))

The set Q consists of the following terms:

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule COND(false, neg(s(z0)), nil) → NTHTAIL(minus_nat(s(0), s(z0)), nil) at position [0] we obtained the following new rules [LPAR04]:

COND(false, neg(s(z0)), nil) → NTHTAIL(minus_nat(0, z0), nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, neg(s(z0)), nil) → NTHTAIL(minus_nat(0, z0), nil)

The TRS R consists of the following rules:

minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))

The set Q consists of the following terms:

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, neg(s(z0)), nil) → NTHTAIL(minus_nat(0, z0), nil)

The TRS R consists of the following rules:

minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))

The set Q consists of the following terms:

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule COND(false, neg(s(z0)), nil) → NTHTAIL(minus_nat(0, z0), nil) at position [0] we obtained the following new rules [LPAR04]:

COND(false, neg(s(s(x0))), nil) → NTHTAIL(neg(s(x0)), nil)
COND(false, neg(s(0)), nil) → NTHTAIL(pos(0), nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ Narrowing

                                                                                                ↳ QDP

                                                                                                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)
COND(false, neg(s(s(x0))), nil) → NTHTAIL(neg(s(x0)), nil)
COND(false, neg(s(0)), nil) → NTHTAIL(pos(0), nil)

The TRS R consists of the following rules:

minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))

The set Q consists of the following terms:

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ Narrowing

                                                                                                ↳ QDP

                                                                                                  ↳ DependencyGraphProof

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, neg(s(s(x0))), nil) → NTHTAIL(neg(s(x0)), nil)
NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)

The TRS R consists of the following rules:

minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))

The set Q consists of the following terms:

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ Narrowing

                                                                                                ↳ QDP

                                                                                                  ↳ DependencyGraphProof

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

COND(false, neg(s(s(x0))), nil) → NTHTAIL(neg(s(x0)), nil)
NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)

R is empty.
The set Q consists of the following terms:

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ Narrowing

                                                                                                ↳ QDP

                                                                                                  ↳ DependencyGraphProof

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ QReductionProof

                                                                                                            ↳ QDP

                                                                                                              ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

COND(false, neg(s(s(x0))), nil) → NTHTAIL(neg(s(x0)), nil)
NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [JAR06] the rule NTHTAIL(neg(s(x0)), nil) → COND(false, neg(s(x0)), nil) we obtained the following new rules [LPAR04]:

NTHTAIL(neg(s(s(y_0))), nil) → COND(false, neg(s(s(y_0))), nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ Narrowing

                                                                                                ↳ QDP

                                                                                                  ↳ DependencyGraphProof

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ QReductionProof

                                                                                                            ↳ QDP

                                                                                                              ↳ ForwardInstantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

COND(false, neg(s(s(x0))), nil) → NTHTAIL(neg(s(x0)), nil)
NTHTAIL(neg(s(s(y_0))), nil) → COND(false, neg(s(s(y_0))), nil)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [JAR06] the rule COND(false, neg(s(s(x0))), nil) → NTHTAIL(neg(s(x0)), nil) we obtained the following new rules [LPAR04]:

COND(false, neg(s(s(s(y_0)))), nil) → NTHTAIL(neg(s(s(y_0))), nil)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ IDependencyGraphProof

        ↳ AND

          ↳ IDP

          ↳ IDP

            ↳ UsableRulesProof

              ↳ IDP

                ↳ IDPtoQDPProof

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ RemovalProof

                            ↳ RemovalProof

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ AND

                                        ↳ QDP

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ UsableRulesProof

                                                                            ↳ QDP

                                                                              ↳ QReductionProof

                                                                                ↳ QDP

                                                                                  ↳ Instantiation

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ Narrowing

                                                                                                ↳ QDP

                                                                                                  ↳ DependencyGraphProof

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ QReductionProof

                                                                                                            ↳ QDP

                                                                                                              ↳ ForwardInstantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ ForwardInstantiation

                                                                                                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

NTHTAIL(neg(s(s(y_0))), nil) → COND(false, neg(s(s(y_0))), nil)
COND(false, neg(s(s(s(y_0)))), nil) → NTHTAIL(neg(s(s(y_0))), nil)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.